R:Realizer, i:Id. R-Feasible(R)  R-ds(R;i) = 1of([[R]](i))  x:Id fp Type 

latex

Definitions

x:A. B(x), P  Q, R-ds(R;i), 1of(t), [[R]], Prop, x. t(x), t  T, if b t else f fi, , @i: x:T initially x = v, @i: only L affects x : t, @i: only L sends on (l with tg), @i: with declarations ds:dsda:daeffect of k(v) is x := f s v, @i: with declarations ds:dsda:da k(v) sends f s v on link l, @i (with ds: ds action a:T precondition a(v) is P s v), @i: k affects only members of L, @i: k sends only links in L, @i: only members of L read x, , mk-ma, x : t initially x = v, true, false, only members of L affect x :t, only L sends on (l with tg), with declarations ds:dsda:daeffect of k(v) is x := f s v, with declarations ds:dsda:dak(v) sends f s v on link l, (with ds: ds action a:T precondition a(v) is P s v), k affects only members of L, k sends only on links in L, only members of L read x, A  B, M1  M2, T, True, x(s), {T}, MsgA, , Unit, P  Q, P & Q, A, False, R-Feasible(R), Dsys, a = b,

Lemmas

es realizer-induction, Id wf, R-Feasible wf, fpf wf, R-ds wf, R-Dsys wf, msga wf, es realizer wf, fpf-empty wf, Rnone wf, eq id wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert-eq-id, fpf-single wf, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, Rinit wf, Rframe wf, Knd wf, lsrc wf, Rsframe wf, IdLnk wf, Reffect wf, decl-state wf, decl-type wf, Rsends wf, Rpre wf, Raframe wf, Rbframe wf, Rrframe wf, fpf-join wf, squash wf, true wf, deq wf, id-deq wf